predicate\_implies($T$;$P_{1}$;$P_{2}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$. ($P_{1}$($x$)) $\Rightarrow$ ($P_{2}$($x$))